$\forall$$a$,$b$:int\_nzero. nequal($\mathbb{Z}$; ($a$ $\ast$ $b$); 0)